
; Copyright (c) 2015 Microsoft Corporation


(simplify (bvshl #x00ff #x0004))
(simplify (bvshl #x00ff #x0008))
(simplify (bvshl #x00ff #x0000))
(simplify (bvshl #x00aa00bb00cc00dd #x0000000000000000))
(simplify (bvshl #x00aa00bb00cc00dd #x0000000000000008))
(simplify (bvshl #x00aa00bb00cc00dd #x0000000000000010))
(simplify (bvshl #x00aa00bb00cc00dd #x0000000000000020))
(simplify (bvshl #x00aa00bb00cc00dd #x0000000000000030))
(simplify (bvshl #x00aa00bb00cc00dd #x000000000000ffff))
(echo "----")
(simplify (bvlshr #x00ff #x0004))
(simplify (bvlshr #x00ff #x0008))
(simplify (bvlshr #x00ff #x0000))
(simplify (bvlshr #x00aa00bb00cc00dd #x0000000000000000))
(simplify (bvlshr #x00aa00bb00cc00dd #x0000000000000008))
(simplify (bvlshr #x00aa00bb00cc00dd #x0000000000000010))
(simplify (bvlshr #x00aa00bb00cc00dd #x0000000000000020))
(simplify (bvlshr #x00aa00bb00cc00dd #x0000000000000030))
(simplify (bvlshr #x00aa00bb00cc00dd #x000000000000ffff))
(echo "----")
(simplify (bvashr #x00ff #x0004))
(simplify (bvashr #x00ff #x0008))
(simplify (bvashr #x00ff #x0000))
(simplify (bvashr #x00aa00bb00cc00dd #x0000000000000000))
(simplify (bvashr #x00aa00bb00cc00dd #x0000000000000008))
(simplify (bvashr #x00aa00bb00cc00dd #x0000000000000010))
(simplify (bvashr #x00aa00bb00cc00dd #x0000000000000020))
(simplify (bvashr #x00aa00bb00cc00dd #x0000000000000030))
(simplify (bvashr #x00aa00bb00cc00dd #x000000000000ffff))
(echo "----")
(simplify (bvashr #x80ff #x0004))
(simplify (bvashr #x80ff #x0008))
(simplify (bvashr #x80ff #x0000))
(simplify (bvashr #x80aa00bb00cc00dd #x0000000000000000))
(simplify (bvashr #x80aa00bb00cc00dd #x0000000000000008))
(simplify (bvashr #x80aa00bb00cc00dd #x0000000000000010))
(simplify (bvashr #x80aa00bb00cc00dd #x0000000000000020))
(simplify (bvashr #x80aa00bb00cc00dd #x0000000000000030))
(simplify (bvashr #x80aa00bb00cc00dd #x000000000000ffff))
(echo "----")

(define-sort W () (_ BitVec 16))
(declare-const c1 W)
(declare-const c2 W)
(simplify (bvashr (bvashr c1 #x0002) #x0003))
(simplify (bvashr (bvashr c1 #x0008) #x0009))
(simplify (bvashr c1 #x0000))
(simplify (bvlshr (bvlshr c1 #x0002) #x0003))
(simplify (bvlshr (bvlshr c1 #x0008) #x0009))
(simplify (bvlshr c1 #x0010))
(simplify (bvlshr c1 #x0000))
(simplify (bvshl (bvshl c1 #x0002) #x0003))
(simplify (bvshl (bvshl c1 #x0008) #x0009))
(simplify (bvshl c1 #x0010))
(simplify (bvshl c1 #x0000))